sv, av, dis, cl, fr, sfr, rfr, afr, bfr, A, B:Top.
R-FeasibleWitness{i:l}
R-FeasibleWitness((A  B); sv; av; dis; cl; fr; sfr; rfr; afr; bfr)
~
(R-FeasibleWitness{i:l}
(R-FeasibleWitness(A; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)
& R-FeasibleWitness{i:l}
& R-FeasibleWitness(B; sv; av; dis; cl; fr; sfr; rfr; afr; bfr)) 

latex

Definitions	t  T, R-FeasibleWitness, x:A. B(x)
Lemmas	top wf